Step of Proof: nat_well_founded 9,38

Inference at * 1 
Iof proof for Lemma nat well founded:



  P:(). (j:. (k:. (k < j P(k))  P(j))  {n:P(n)} 
latex

 by ((RepD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 
latex


C1

C1: 1. P : 
C1: 2. j:. (k:. (k < j P(k))  P(j)
C1:   n:P(n)
C.


Definitionst  T, {T}, x(s), P  Q, , x:AB(x),
Lemmasnat wf

origin